COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	basic properties of reverse and rev
C00004 00003	proofs of facts on reverse
C00011 ENDMK
C⊗;
;basic properties of reverse and rev
;the properties listed as axioms here will be proved on the next pages

(wipe-out) 
(get-proofs lispax prf ekl sys)
(proof reverse)

(decl reverse (unaryname: reverse) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl rev (type: |ground⊗ground→ground|) (syntype: constant))

(define rev |∀x u v.rev(nil,v)=v∧rev(x.u,v)=rev(u,x.v)|
	(use listinductiondef))
(label revdef)
(label simpinfo)

(axiom |∀u v.rev(u,v)=reverse u*v|)
(label revprop)

(define reverse |∀x u.reverse(nil)=nil∧reverse(x.u)=(reverse u)*(x.nil)|
       (use listinductiondef))
(label reversedef) (label simpinfo)

(axiom |∀u.reverse u = rev(u,nil)|)
(label reverserev)

(axiom |∀u.listp reverse u|)
(label reverselist) (label simpinfo)

(axiom |∀x.reverse (x.nil)=x.nil|)
(label simpinfo)

(axiom |∀u.reverse reverse u = u|)
(label simpinfo)
(label reversereverse)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)
(label reverseappend)

(save-proofs reverse)
;proofs of facts on reverse
;13s cpu
(wipe-out) 
(get-proofs reverse prf ekl sys)
(proof revprops)

;remove reverse facts from simpinfo so we don't use it accidentally

(unlabel simpinfo reversereverse)
(unlabel simpinfo reverselist)

;termination

(ue (phi |λu.listp reverse u|) listinduction (open reverse))
;∀U.LISTP REVERSE U
(label simpinfo)

;proof of reverseappend
(ue (phi |λu.(reverse (u*v) = reverse(v) * reverse(u))|) listinduction
    (open reverse))
;∀U.REVERSE (U*V)=REVERSE V*REVERSE U

;proof of reversereverse from reverseappend

(ue (phi |λu.reverse (reverse u) = u|) listinduction
    (open reverse) (use reverseappend mode: always))
;∀U.REVERSE (REVERSE U)=U

(ue (phi |λu.∀v w.rev(u,v)*w=rev(u,v*w)|) listinduction)
;(∀X U.(∀V W.REV(U,V)*W=REV(U,V*W))⊃(∀V W.REV(U,X.V)*W=REV(U,X.(V*W))))⊃
;(∀U V W.REV(U,V)*W=REV(U,V*W))
(label revapp1)

(assume |∀V W.REV(U,V)*W=REV(U,V*W)|)
(label revapp2)

(tci (revapp2) |∀V W.REV(U,X.V)*W=REV(U,(X.V)*W)| (use revapp2))
;(∀V W.REV(U,V)*W=REV(U,V*W))⊃(∀V W.REV(U,X.V)*W=REV(U,X.V*W))

(rw revapp1 (use *))
;∀U V W.REV(U,V)*W=REV(U,V*W)
(label revapp)

(ue (phi |λu.∀v.(rev(u,v)=reverse(u)*v)|)
    listinduction
    (open reverse) (use revapp mode: always))
;∀U V.REV(U,V)=REVERSE U*V

(ue (v nil) *)
;∀U.REV(U,NIL)=REVERSE U